\begin{tabbing}
$\forall$\=$E$, $X_{1}$, $X_{2}$:Type, ${\it dE}$:EqDecider($E$), ${\it dL}$:EqDecider(IdLnk), ${\it pred?}$:($E$$\rightarrow$(?$E$)),\+
\\[0ex]${\it info}$:($E$$\rightarrow$((:Id $\times$ $X_{1}$) + (:(:IdLnk $\times$ $E$) $\times$ $X_{2}$))),
\\[0ex]$p$:(\=$\forall$$e$:$E$, $l$:IdLnk.\+
\\[0ex]$\exists$\=${\it e'}$:$E$\+
\\[0ex]($\forall$${\it e''}$:$E$.
\\[0ex]($\uparrow$rcv?(${\it e''}$))
\\[0ex]$\Rightarrow$ (sender(${\it e''}$) = $e$)
\\[0ex]$\Rightarrow$ (link(${\it e''}$) = $l$)
\\[0ex]$\Rightarrow$ (((${\it e''}$ = ${\it e'}$) $\vee$ ${\it e''}$ $<$ ${\it e'}$) \& loc(${\it e'}$) = destination($l$) $\in$ Id))).
\-\-\-\\[0ex]SWellFounded(pred!($e$;${\it e'}$))
\\[0ex]$\Rightarrow$ ($\forall$$e$:$E$. ($\neg$($\uparrow$first($e$))) $\Rightarrow$ (loc(pred($e$)) = loc($e$) $\in$ Id))
\\[0ex]$\Rightarrow$ ($\forall$$e$, ${\it e'}$:$E$. (loc($e$) = loc(${\it e'}$) $\in$ Id) $\Rightarrow$ (${\it pred?}$($e$) = ${\it pred?}$(${\it e'}$)) $\Rightarrow$ ($e$ = ${\it e'}$))
\\[0ex]$\Rightarrow$ \=($\forall$$e$:$E$, $l$:IdLnk, $n$:\{0..$\parallel$receives(${\it dE}$;${\it dL}$;${\it pred?}$;${\it info}$;$p$;$e$;$l$)$\parallel^{-}$\}.\+
\\[0ex]$\exists$\=${\it e'}$:$E$\+
\\[0ex](($\uparrow$rcv?(${\it e'}$))
\\[0ex]c$\wedge$ (link(${\it e'}$) = $l$ \& sender(${\it e'}$) = $e$ \& index(${\it dE}$;${\it dL}$;${\it pred?}$;${\it info}$;$p$;${\it e'}$) = $n$ $\in$ $\mathbb{Z}$)))
\-\-
\end{tabbing}